General choice

• L1 <[]-idem>              P [] P = P;
• L2 <[]-sym>               P [] Q = Q [] P
• L3 <[]-assoc>            P [] (Q [] R) = (P [] Q) [] R
• L4 <[]-unit>                Stop [] P = P

Internal choice

• L1 <<>-sym>           P <> Q = Q <> P
• L2 <<>-assoc>        P <> (Q <> R) = (P <> Q) <> R

Sequential composition

• L1 <; -dist-l>             (P <> Q); R = (P;R) <> (Q;R)
• L2 <; -assoc>           P; (Q; R) = (P; Q); R
• L3 <; -unit-l>             Skip; P = P
• L4 <; -unit-r>             P; Skip = P

Parallel composition

• L1 <||-1>                   a -> P || a -> Q = a -> (P||Q), given that a  (P   
• L2 <||-2>                   a -> P || b -> Q = Stop, given that a, b  (P Q) and a  b
• L3 <||-3>                   a -> P || b -> Q = b -> (a -> P || Q), given that a  (P    Q) and b (P   
• L4 <||-4>                   a -> P || b -> Q = a -> (P || b -> Q) [] b -> (a -> P || Q), given that a, b (P   
• L5 <||-sym>              P || Q = Q || P
• L6 <||-assoc>           P || Q || R = P || (Q || R)
• L7 <||-termination-1>    Skip || Skip = Skip
• L8 <||-termination-2>    Skip || Stop = Stop

Interleaving

• L1 <|||-sym>                P ||| Q = Q ||| P
• L2 <|||-assoc>            (P|||Q) |||R = P ||| (Q ||| R)
• L3 <|||-unit>                Skip ||| P = P

Hiding

• L1 <hide-dist>            (P <> Q)\X = (P\X) <> (Q\X)
• L2 <hide-sym>           (P\Y)\X = (P\X)\Y
• L3 <hide-combine>   (P\Y)\X = P\(X Y)
• L4 <null hiding>          P\{} = P
• L5 <hide-step>          
• L6 <Skip-hide>          Skip \X = Skip